/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Vector;

import salvo.jesus.graph.DirectedAcyclicGraph;
import salvo.jesus.graph.DirectedAcyclicGraphImpl;
import salvo.jesus.graph.DirectedEdge;
import salvo.jesus.graph.Edge;
import salvo.jesus.graph.Vertex;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.util.Dbg;
import alloy.util.Msg;


/** 
 * visitor which constructs extends graph for signatures
 */

public class ConstructExtendsGraphVisitor extends ASTDepthFirstVisitor {

    /** DAG representing extends graph */
    public DirectedAcyclicGraph extendsDAG = new DirectedAcyclicGraphImpl();

    /**
     * mapping from {@link String} qualified sig names to {@link Vertex} vertices
     * corresponding to the signatures
     */
    private Map _nameToVertex = new HashMap();

    /** current module scope */
    private ModuleInfo _curModuleInfo;


    /**
     * set the current module scope and visit the
     * signatures
     * @param module_ the Module
     */
    public void visit(Module module_) {
        _curModuleInfo = module_.getModuleInfo();
        module_.getSignatures().applyVisitor(this);
    }

    /**
     * create a vertex for the signature if necessary and
     * add edges between it and the sigs it extends.  Also,
     * add parent pointers from the local scope of the
     * signature to the field-holding local scope of its parent
     * signatures.
     * @param signature_ the Signature
     */
    public void visit(Signature signature_) {
        Vertex sigVertex = getSigVertex(signature_);

        // iterate through signatures that signature_ extend or is a subset of
	// the algorithm is the same for both . . .

	Iterator extended = null;
	if (signature_.isSubset())
	    extended = signature_.getSubsets().getSigExprIter();
	else
	    extended = signature_.getExtends().getSigExprIter();

        while (extended.hasNext()) {
            SigExpr extensionExpr = (SigExpr)extended.next();
	    Vertex extendedSigVertex = getExtendedSigVertex(extensionExpr);
	    if (extendedSigVertex == null) return;
	    // see if the extended signature is extended twice by checking for
	    // an existing edge in the graph
	    DirectedEdge existingEdge = extendsDAG.getEdge(sigVertex, extendedSigVertex);
	    if (existingEdge != null) {
		Dbg.user(new Msg("signature already extended", extensionExpr));
	    } else {
		Edge addedEdge = extendsDAG.addEdge(sigVertex, extendedSigVertex);
		// check for cycles by checking if the added edge is null
		if (addedEdge == null) {
		    Dbg.user(new Msg("cyclic extension", extensionExpr));
		} else {
		    // also, make the field local scope of the parent signature
		    // a parent of the field local scope of signature_
		    
		    LocalScope curFieldLocalScope = signature_.getLocalScope();
		    LocalScope parScope = ((Signature)extendedSigVertex.getObject()).getLocalScope();
		    while (parScope.getBoundNames().hasNext()) {
			curFieldLocalScope.addParent(parScope);
		    }
		}
	    }
        }
    }

    

  
    /**
     * Get a list of the signatures sorted so that no signature appears
     * before a signature it extends.  This method should be called after
     * the visitor is applied to the specification, as it creates the sorted
     * list by doing a reverse topological sort on the constructed graph.
     * @return the sorted list of signatures
     */
    public List getSortedSigs() {
        Vector sort = extendsDAG.reverseTopologicalSort();
        List sigs = new ArrayList();
        Iterator vertices = sort.iterator();
        while (vertices.hasNext()) {
            Vertex v = (Vertex)vertices.next();
            sigs.add(v.getObject());
        }
        return sigs;
    }
        
    /**
     * get the vertex for an extended signature, creating it
     * if necessary
     * @param sigExpr_ the SigExpr found in the extends clause
     * @return the Vertex
     */
    private Vertex getExtendedSigVertex(SigExpr sigExpr_) { 
        QualifiedName extendedSigName = sigExpr_.getSig();
        Signature extendedSignature = _curModuleInfo.getSignature(extendedSigName, "extend");
        return (extendedSignature == null) ? null : getSigVertex((Signature)extendedSignature);
    }
                
    /**
     * return the existing vertex for a signature if it has
     * been created, or a new vertex if it has not been created
     * @param signature_ the Signature
     * @return the new Vertex
     */
    private Vertex getSigVertex(Signature signature_) {
        // see if a node has already been created for the signature
        String sigName = signature_.getName().nodeString();
        Vertex sigVertex = null;
        if (_nameToVertex.containsKey(sigName)) {
            sigVertex = (Vertex)_nameToVertex.get(sigName);
        } else {
            // construct a new vertex and add it to the mapping
            // and graph
            sigVertex = new Vertex(signature_);
            _nameToVertex.put(sigName, sigVertex);
            extendsDAG.add(sigVertex);
        }
        return sigVertex;
    }


}
    
